\documentclass{article}
\usepackage{url}
\usepackage{manfnt}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{xcolor}
\usepackage{mathrsfs}
\usepackage{amsmath, amsthm}

\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}
% My own macros

\newcommand{\ep}[0]{\epsilon} 
\newcommand{\nil}[0]{\mathsf{nil}} 
\newcommand{\cons}[0]{\mathsf{cons}} 
\newcommand{\vecc}[0]{\mathsf{vec}} 
\newcommand{\suc}[0]{\mathsf{S}} 
\newcommand{\app}[0]{\mathsf{app}} 
\newcommand{\interp}[1]{\lVert #1 \rVert} 

\newtheorem{prop}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}


\begin{document}
%\pagestyle{empty}
\title{Investigation of System $\mathfrak{G}$}
\author{Peng Fu \\
Computer Science, The University of Iowa}
\date{last edited: \today}


\maketitle
\thispagestyle{empty}
\section{Introduction}
This note try to \textit{justify} system $\mathfrak{G}$. We identify six syntactical categories, namely, \textit{domain term}, \textit{set}\footnote{Do not confused this with the ``set'' in ZFC, here is just a name for a syntactical category}, \textit{formula}, \textit{type}, \textit{proof term}, \textit{pure lambda term}. Let us first see the definition of pure lambda term:

\begin{definition}
\

\noindent \textit{Pure Lambda Terms} $t \ ::= x \ | \ \lambda x.t \ | \ t t'$
\end{definition}
 
\section{Frege's System $\mathfrak{F}$}

\begin{definition}[Syntax]
\

\noindent \textit{Domain Terms/Set} $b \ :: = \ u \ | \ \iota u.F$

\noindent \textit{Formula/Type} $F \ ::= \bot \ | \ X \ | \ b \ep b' \ | \ \Pi X.F \ | \ \ F_1 \to F_2 \ | \ \forall u.F$

\noindent \textit{Proof Terms} $p \ ::= \ a \ | \ \lambda a .p \ | \ p p'$

\noindent \textit{Proof Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, a : F$

\end{definition} 

%% \begin{definition}[Metalevel Abrieviation]
%% \

%%   \noindent \textit{Objects} $o \ ::= \ t \ | \ T$

%%   \noindent \textit{Reduction Context} $\mathcal{C} \ ::=$

%% \noindent $ \bullet \ | \ \lambda x.\mathcal{C} \ | \ \mathcal{C} t'\ | \ t \mathcal{C}\ |\ \Delta X:\kappa.\mathcal{C} \ | \ \Pi x:T .\mathcal{C} \ |\ \Pi x:\mathcal{C}.T \ | \  \forall x:T .\mathcal{C} \ |\ \forall x:\mathcal{C}.T \ | \ \lambda X.\mathcal{C} \ | \ \iota x.\mathcal{C} \ | \ T \mathcal{C} \ | \ \mathcal{C} T \ | \ \xi x:\mathcal{C}.\kappa \ | \  \zeta X:\mathcal{C}. \kappa \ | \ \xi x:\kappa.\mathcal{C} \ | \  \zeta X:\kappa. \mathcal{C}$

%% \end{definition}

\begin{definition}[Typing Rules]
\

\footnotesize{
\begin{tabular}{lll}
    
\infer[\textit{Var}]{\Gamma \vdash a:F}{(a:F) \in \Gamma}

&
\infer[\textit{Conv}]{\Gamma \vdash p : F_2}{\Gamma \vdash p:
F_1 &  F_1 \cong F_2}

&

\infer[\textit{Forall}]{\Gamma \vdash p : \forall u.F}
{\Gamma \vdash p: F &  u \notin \mathsf{FV}(\Gamma)}

\\
\\
\infer[\textit{Instantiate}]{\Gamma \vdash p :[b/u]F}{\Gamma
\vdash p: \forall u.F}

&

\infer[\textit{Poly}]{\Gamma \vdash  p :\Pi X.F}
{\Gamma \vdash p: F & X \notin \mathsf{FV}(\Gamma)}

&
\infer[\textit{Inst}]{\Gamma \vdash p:[F'/X]F}{\Gamma \vdash p: \Pi X.F}

\\
\\

\infer[\textit{Func}]{\Gamma \vdash \lambda a.p : F_1\to F_2}
{\Gamma, a:F_1 \vdash p: F_2}

&

\infer[\textit{App}]{\Gamma \vdash p p':F_2}{\Gamma
\vdash p: F_1 \to F_2 & \Gamma \vdash p': F_1}

\end{tabular}
}
\end{definition}

\noindent \textbf{Note}: $\cong$ is defined as reflexive transitve and symmetric closure of 
$\to_{c}$.
\begin{definition}[Comprehension, proof reductions]

\


\begin{tabular}{ll}

\infer{ b \ep (\iota u.F) \to_{c} [b/u]F}{}

&

\infer{(\lambda a.p)p' \to_{\beta} [p'/a]p}{}

\end{tabular}
  
\end{definition}

\noindent \textbf{Remarks}: 
\

\begin{itemize}
\item We just use Curry-Howard correspondent to structure an intuitionistic version of
Frege's system. $\neg F := F \to \bot$. 
\item This system is undesirable in the sense that both $(\iota u_1. u_1 \not \in u_1) \not \in (\iota u_1. u_1 \not \in u_1) \leftrightarrow  (\iota u_1. u_1 \not \in u_1) \ep (\iota u_1. u_1 \not \in u_1)$ are provable in system $\mathfrak{F}$.

\item Because in an intuitionistic system, we cannot further exploit above fact to get inconsistency, but still, it limits the possibility to have an classical extension. 

\end{itemize}


\section{Girard's System $\mathbf{F}$}

\begin{definition}[Syntax]
\

\noindent \textit{Formula/Type} $F \ ::= \ X \ | \ \Pi X.F \ | \ \ F_1 \to F_2$

\noindent \textit{Proof Terms} $p \ ::= \ a \ | \ \lambda a .p \ | \ p p'$

\noindent \textit{Proof Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, a : F$

\end{definition} 

\begin{definition}[Typing Rules]
\

\footnotesize{
\begin{tabular}{lll}
    
\infer[\textit{Var}]{\Gamma \vdash a:F}{(a:F) \in \Gamma}

&

\infer[\textit{Poly}]{\Gamma \vdash  p :\Pi X.F}
{\Gamma \vdash p: F & X \notin \mathsf{FV}(\Gamma)}

&
\infer[\textit{Inst}]{\Gamma \vdash p:[F'/X]F}{\Gamma \vdash p: \Pi X.F}

\\
\\

\infer[\textit{Func}]{\Gamma \vdash \lambda a.p : F_1\to F_2}
{\Gamma, a:F_1 \vdash p: F_2}

&

\infer[\textit{App}]{\Gamma \vdash p p':F_2}{\Gamma
\vdash p: F_1 \to F_2 & \Gamma \vdash p': F_1}

\end{tabular}
}
\end{definition}

\section{Second Order Intuitionistic Logic $\mathbf{SIL}$}

\begin{definition}[Syntax]
\

\noindent \textit{Domain Terms} $b \ :: = u \ | \ f^n(b_1,..., b_n)$

\noindent \textit{Formula/Type} $F \ ::= X \ | \ R^n(b_1,...,b_n) \ | \ \Pi X.F \ | \ \ F_1 \to F_2 \ | \ \forall u.F$

\noindent \textit{Proof Terms} $p \ ::= \ a \ | \ \lambda a .p \ | \ p p'$

\noindent \textit{Proof Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, a : F$

\end{definition} 

\begin{definition}[Typing Rules]
\

\footnotesize{
\begin{tabular}{lll}
    
\infer[\textit{Var}]{\Gamma \vdash a:F}{(a:F) \in \Gamma}

&
\infer[\textit{Conv}]{\Gamma \vdash p : F_2}{\Gamma \vdash p:
F_1 &  F_1 \cong F_2}

&

\infer[\textit{Forall}]{\Gamma \vdash p : \forall u.F}
{\Gamma \vdash p: F &  u \notin \mathsf{FV}(\Gamma)}

\\
\\
\infer[\textit{Instantiate}]{\Gamma \vdash p :[b/u]F}{\Gamma
\vdash p: \forall u.F}

&

\infer[\textit{Poly}]{\Gamma \vdash  p :\Pi X.F}
{\Gamma \vdash p: F & X \notin \mathsf{FV}(\Gamma)}

&
\infer[\textit{Inst}]{\Gamma \vdash p:[F'/X]F}{\Gamma \vdash p: \Pi X.F}

\\
\\

\infer[\textit{Func}]{\Gamma \vdash \lambda a.p : F_1\to F_2}
{\Gamma, a:F_1 \vdash p: F_2}

&

\infer[\textit{App}]{\Gamma \vdash p p':F_2}{\Gamma
\vdash p: F_1 \to F_2 & \Gamma \vdash p': F_1}

\end{tabular}
}
\end{definition}

\section{System $\mathfrak{G}_0$}

\begin{definition}[Syntax]
\

\noindent \textit{Domain Terms/Pure Lambda Terms} $t \ ::= x \ | \ \lambda x.t \ | \ t t'$

\noindent \textit{Set/Formula/Type} $F \ ::=  \ X \ | \ \iota x.F \ | \ t \ep F \ | \ \Pi X.F \ | \ \ F_1 \to F_2 \ | \ \forall x.F$

\noindent \textit{Proof Terms} $p \ ::= \ a \ | \ \lambda a .p \ | \ p p'$

\noindent \textit{Proof Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, a : F$

\end{definition} 

\begin{definition}[Typing Rules]
\

\footnotesize{
\begin{tabular}{lll}
    
\infer[\textit{Var}]{\Gamma \vdash a:F}{(a:F) \in \Gamma}

&
\infer[\textit{Conv}]{\Gamma \vdash p : F_2}{\Gamma \vdash p:
F_1 &  F_1 \cong F_2}

&

\infer[\textit{Forall}]{\Gamma \vdash p : \forall x.F}
{\Gamma \vdash p: F &  x \notin \mathsf{FV}(\Gamma)}

\\
\\
\infer[\textit{Instantiate}]{\Gamma \vdash p :[t/x]F}{\Gamma
\vdash p: \forall x.F}

&

\infer[\textit{Poly}]{\Gamma \vdash  p :\Pi X.F}
{\Gamma \vdash p: F & X \notin \mathsf{FV}(\Gamma)}

&
\infer[\textit{Inst}]{\Gamma \vdash p:[F'/X]F}{\Gamma \vdash p: \Pi X.F}

\\
\\

\infer[\textit{Func}]{\Gamma \vdash \lambda a.p : F_1\to F_2}
{\Gamma, a:F_1 \vdash p: F_2}

&

\infer[\textit{App}]{\Gamma \vdash p p':F_2}{\Gamma
\vdash p: F_1 \to F_2 & \Gamma \vdash p': F_1}

\end{tabular}
}
\end{definition}

\noindent \textbf{Note}: $\cong$ is defined as reflexive transitve and symmetric closure of 
$\to_{t\beta} \cup \to_{c}$.
\begin{definition}[Comprehension, proof reductions]

\


\begin{tabular}{lll}

\infer{ t \ep (\iota x.F) \to_{c} [t/x]F}{}

&

\infer{(\lambda a.p)p' \to_{\beta} [p'/a]p}{}

&

\infer{(\lambda x.t)t' \to_{t\beta} [t'/x]t}{}

\end{tabular}
  
\end{definition}

\subsection{Church Numerals}

\begin{definition}[Church Numerals]
\

  \noindent $\mathsf{Nat} := \iota x. \Pi C.(\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C  \to x \ep C$

\noindent $\mathsf{S} \ := \lambda n. \lambda s.\lambda z. s \ (n\ s\ z)$

\noindent $0\  := \lambda s. \lambda z.z$

\end{definition}

\begin{definition}[Induction]
\

\noindent  $\mathsf{Id} :  \Pi C. (\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C \to \forall m. (m \ep \mathsf{Nat} \to m \ep C)$

\noindent $\mathsf{Id} := \lambda s. \lambda z. \lambda n. n\ s\ z$

\noindent with $s:\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), z: 0 \ep C, n: m \ep \mathsf{Nat}$.
\end{definition}

\noindent \textbf{Remarks}: 
\begin{itemize}
\item $\mathsf{Id}$ is a proof term. One can prove that $\cdot \vdash p: 0 \ep \mathsf{Nat}$ and $\cdot \vdash p': \forall m. (m \ep \mathsf{Nat} \to \mathsf{S}m \ep \mathsf{Nat})$. 
\item One can prove that(at meta-level) for any Church numeral $\bar{n}$, if $p: \bar{n} \ep \mathsf{Nat}$, then $p$ is alpha equivalent to $\bar{n}$. This suggests that proof terms of type $\bar{n} \ep \mathsf{Nat}$ coincides with pure lambda term $\bar{n}$. 
\end{itemize}

\section{System $\mathfrak{G}_1$}

\begin{definition}
\

\noindent \textit{Formula/Type/Set} $T \ ::= \ X \ | \ \Pi X.T \ | \ \ T_1 \to T_2 \ | \ \forall x.T \ | \ \iota x.T \ | \ t \ep T $

\noindent \textit{Domain Terms/Pure Lambda Terms/Proof Terms} $t \ :: = \ x \ | \ \lambda x.t \ | \ t t'$

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, x:T$

\end{definition} 

\noindent \textbf{Remarks}: 
\begin{itemize}
\item We collapse the syntactical category of formula, type and set. This move is debatable. Now we have quantification over individuals(terms) and quantification over both set and formula. 
\end{itemize}

\begin{definition}[Typing Rules]
\

\footnotesize{
\begin{tabular}{lll}
    
\infer[\textit{Var}]{\Gamma \vdash x:T}{(x:T) \in \Gamma}

&
\infer[\textit{Conv}]{\Gamma \vdash t : T_2}{\Gamma \vdash t:
T_1 &  T_1 \cong T_2}

&

\infer[\textit{Forall}]{\Gamma \vdash t : \forall x.T}
{\Gamma \vdash t: T &  x \notin \mathsf{FV}(\Gamma)}

\\
\\
\infer[\textit{Instantiate}]{\Gamma \vdash t :[t'/x]T_2}{\Gamma
\vdash t: \forall x.T}
&

\infer[\textit{Poly}]{\Gamma \vdash  t :\Pi X.T}
{\Gamma \vdash t: T & X \notin \mathsf{FV}(\Gamma)}

&
\infer[\textit{Inst}]{\Gamma \vdash t:[T'/X]T}{\Gamma \vdash t: \Pi X.T}

\\
\\

\infer[\textit{Func}]{\Gamma \vdash \lambda x.t : T_1\to T_2}
{\Gamma, x:T_1 \vdash t: T_2}

&

\infer[\textit{App}]{\Gamma \vdash t t':T_2}{\Gamma
\vdash t: T_1 \to T_2 & \Gamma \vdash t': T_1}

\end{tabular}
}
\end{definition}

\noindent \textbf{Note}: $\cong$ is defined as reflexive transitve and symmetric closure of 
$\to_{\beta}\cup \to_{\iota}$.
\begin{definition}[Beta Reductions]

\


\begin{tabular}{ll}

\infer{(\lambda x.t)t' \to_{\beta} [t'/x]t}{}

&

\infer{t \ep (\iota x.T) \to_{\iota} [t/x]T}{}

\end{tabular}
  
\end{definition}

\section{System $\mathfrak{G}_2$}

\begin{definition}
\

\noindent \textit{Formula/Type} $T \ ::= \  X^0 \ | \ t \ep S \ | \ \Pi X^1.T \ | \ \ T_1 \to T_2 \ | \ \forall x.T \ | \ \Pi X^0.T$ 

\noindent \textit{Set} $S \ ::= X^1 \ | \ \iota x.T$

\noindent \textit{Domain Terms/Pure Lambda Terms} $t \ :: = \ x \ | \ \lambda x.t \ | \ t t'$

\noindent \textit{Proof Terms} $p \ ::= \ a \ | \ \lambda a .p \ | \ p p'$

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, a:T$

\end{definition} 

\noindent \textbf{Remarks}: 
\begin{itemize}
\item
\end{itemize}

\begin{definition}[Typing Rules]
\

\footnotesize{
\begin{tabular}{lll}
    
\infer[\textit{Var}]{\Gamma \vdash a:T}{(a:T) \in \Gamma}

&
\infer[\textit{Conv}]{\Gamma \vdash p : T_2}{\Gamma \vdash p:
T_1 &  T_1 \cong T_2}

&

\infer[\textit{Forall}]{\Gamma \vdash p : \forall x.T}
{\Gamma \vdash p: T &  x \notin \mathsf{FV}(\Gamma)}

\\
\\
\infer[\textit{Instantiate}]{\Gamma \vdash p :[t'/x]T_2}{\Gamma
\vdash p: \forall x.T}
&

\infer[\textit{Poly}]{\Gamma \vdash  p :\Pi X^i.T}
{\Gamma \vdash p: T & X^i \notin \mathsf{FV}(\Gamma) & i= 0,1}

&
\infer[\textit{Inst0}]{\Gamma \vdash p:[T'/X^0]T}{\Gamma \vdash p: \Pi X^0.T}

\\
\\

\infer[\textit{Func}]{\Gamma \vdash \lambda a.p : T_1\to T_2}
{\Gamma, a:T_1 \vdash p: T_2}

&

\infer[\textit{App}]{\Gamma \vdash p p':T_2}{\Gamma
\vdash p: T_1 \to T_2 & \Gamma \vdash p': T_1}

&


\infer[\textit{Inst1}]{\Gamma \vdash p:[S/X^1]T}{\Gamma \vdash p: \Pi X^1.T}

\end{tabular}
}
\end{definition}

\noindent \textbf{Note}: $\cong$ is defined as reflexive transitve and symmetric closure of 
$\to_{\beta}\cup \to_{\iota}$.
\begin{definition}[Beta Reductions]

\


\begin{tabular}{ll}

\infer{(\lambda x.t)t' \to_{\beta} [t'/x]t}{}

&

\infer{t \ep (\iota x.T) \to_{\iota} [t/x]T}{}

\end{tabular}
  
\end{definition}

\section{System $\mathfrak{G}_3$}

\begin{definition}
\

\noindent \textit{Formula/Type} $T \ ::= \  X^0 \ | \ t \ep S \ | \ \Pi X^1.T \ | \ \ T_1 \to T_2 \ | \ \forall x.T \ | \ \Pi X^0.T$ 

\noindent \textit{Set/Objects} $S \ ::= X^1 \ | \ \iota x.T$

\noindent \textit{Morphism} $M \ ::= t \ep S \ | \ \forall x.(x\ep S \to M)$

\noindent \textit{Domain Terms/Pure Lambda Terms} $t \ :: = \ x \ | \ \lambda x.t \ | \ t t'$

\noindent \textit{Proof Terms} $p \ ::= \ a \ | \ \lambda a .p \ | \ p p'$

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, a:T$

%\noindent \textit{Records} $\Delta \ :: = \ \cdot \ | \ \Delta, a: x \ep S$

\end{definition} 

\begin{definition}[Typing Rules]
\

\footnotesize{
\begin{tabular}{lll}
    
\infer[\textit{Var}]{\Gamma \vdash a:T}{(a:T) \in \Gamma}

&
\infer[\textit{Conv}]{\Gamma \vdash p : T_2}{\Gamma \vdash p:
T_1 &  T_1 \cong T_2}

&

\infer[\textit{Forall}]{\Gamma \vdash p : \forall x.T}
{\Gamma \vdash p: T &  x \notin \mathsf{FV}(\Gamma)}

\\
\\
\infer[\textit{Instantiate}]{\Gamma \vdash p :[t'/x]T_2}{\Gamma
\vdash p: \forall x.T}
&

\infer[\textit{Poly}]{\Gamma \vdash  p :\Pi X^i.T}
{\Gamma \vdash p: T & X^i \notin \mathsf{FV}(\Gamma) & i= 0,1}

&
\infer[\textit{Inst0}]{\Gamma \vdash p:[T'/X^0]T}{\Gamma \vdash p: \Pi X^0.T}

\\
\\

\infer[\textit{Func}]{\Gamma \vdash \lambda a.p : T_1\to T_2}
{\Gamma, a:T_1 \vdash p: T_2}

&

\infer[\textit{App}]{\Gamma \vdash p p':T_2}{\Gamma
\vdash p: T_1 \to T_2 & \Gamma \vdash p': T_1}

&


\infer[\textit{Inst1}]{\Gamma \vdash p:[S/X^1]T}{\Gamma \vdash p: \Pi X^1.T}

\end{tabular}
}
\end{definition}

\noindent \textbf{Note}: $\cong$ is defined as reflexive transitve and symmetric closure of 
$\to_{\beta}\cup \to_{\iota}$.

\begin{definition}[Functional Extensionality and Comprehension]

\


\begin{tabular}{ll}

\infer{(\lambda x.t)t' \to_{\beta} [t'/x]t}{}

&

\infer{t \ep (\iota x.T) \to_{\iota} [t/x]T}{}

\end{tabular}
  
\end{definition}

\begin{definition}[Internal Language]
\

\begin{tabular}{llll}
    
\infer{\Gamma \vdash a: x \ep S}{a: (x\ep S) \in \Gamma }

&

\infer{\Gamma \vdash \lambda a.p : \forall x.(x\ep S \to M)}
{\Gamma, a: x\ep S \vdash p: M}

&

\infer{\Gamma \vdash p p':[t'/x]M}{\Gamma
\vdash p: \forall x.(x \ep S \to M) & \Gamma \vdash p': t' \ep S}

&


%% \infer{\Delta \vdash \lambda y.[t/x]t':S_1 \longrightarrow S_3}{\Delta
%% \vdash \lambda y.t: S_1 \longrightarrow S_2 & \Delta \vdash \lambda x.t': S_2 \longrightarrow S_3}

\end{tabular}

\end{definition}

One can observe that the language of categorization is a sublanguage of typing. The notion 
of morphism is nothing but a fragment of the formula/type. Now let us reduce system $\mathfrak{G}$ to $\mathfrak{G}_3$. 

\begin{definition}[Church Numerals]
\

  \noindent $\mathsf{Nat} := \iota x. \Pi C^1.(\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C  \to x \ep C$

\noindent $\mathsf{S} \ := \lambda n. \lambda s.\lambda z. s \ (n\ s\ z)$

\noindent $0\  := \lambda s. \lambda z.z$

\end{definition}

\begin{definition}
\

\noindent $\bar{0}:= \lambda a.\lambda b.b: 0 \ep \mathsf{Nat}$

\noindent $\bar{\suc}:= \lambda c.\lambda a.\lambda b. a\ (c\ a\ b): \forall x.(x \ep \mathsf{Nat} \to \suc x \ep \mathsf{Nat})$

\noindent with $a :\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), b: 0 \ep C, c: x\ep \mathsf{Nat}$. 
  
\end{definition}


\begin{definition}[Induction]
\

\noindent  $\mathsf{Ind} :  \Pi C^1. (\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C \to \forall m. (m \ep \mathsf{Nat} \to m \ep C)$

\noindent $\mathsf{Ind} := \lambda a. \lambda b. \lambda c. c\ a\ b$

\noindent with $a:\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), b: 0 \ep C, c: m \ep \mathsf{Nat}$.
\end{definition}

\begin{definition}
\

\noindent Let $\mathsf{add} := \lambda n.\lambda m. n \ \suc \ m$. 

\noindent  $\forall x. (x \ep \mathsf{Nat} \to \forall y. (y \ep \mathsf{Nat} \to \mathsf{add}\ y \ x \ep \mathsf{Nat}))$ is provable. 
\end{definition}
\begin{proof}
  Assume $a: x \ep \mathsf{Nat}$. Let $P:= \iota z. \mathsf{add} z\ x \ep \mathsf{Nat}$. Instantiate $C^1$ in $\mathsf{Ind}$ with $P$, we get $(\forall y . ( (\mathsf{add}\ y\ x \ep \mathsf{Nat}) \to \mathsf{add}\  (\mathsf{S} y)\ x \ep \mathsf{Nat})) \to \mathsf{add}\ 0\ x \ep \mathsf{Nat} \to \forall m. (m \ep \mathsf{Nat} \to \mathsf{add}\ m\ x \ep \mathsf{Nat})$. Base case is by assumption. For step case, assume $b: \mathsf{add}\ y\ x \ep \mathsf{Nat} \equiv y\ \suc\ x\ep \mathsf{Nat}$, we want to show $\mathsf{add}\  (\mathsf{S} y)\ x \ep \mathsf{Nat} \equiv \mathsf{S}\ (y\ \suc \ x) \ep \mathsf{Nat}$. This is by $\bar{\suc}$. So the proof term will be
$\bar{+}:= \lambda a. \mathsf{Ind}\ (\lambda b.\bar{\suc}b)\ a$. 
\end{proof}

\noindent One can use internal language to prove this, which is way easier, in that case 
$\bar{+}:= \lambda d. \lambda c. c\ (\lambda q.\bar{\suc}q)\ d$.


\section{Understanding Formula-Set Reciprocity}

\begin{definition}[Internal Functional Language]
\

\begin{tabular}{lll}
    
\infer{\Xi \Vdash x :: U}{x::U \in \Xi }

&

\infer{\Xi \Vdash \lambda x.t :: \Pi x:U. U'}
{\Xi, x:: U \Vdash t :: U'}

&

\infer{\Xi \Vdash t t' ::[t'/x]U}{\Xi
\Vdash t::  \Pi x: U'.U & \Xi \Vdash t':: U'}

\\
\\

\infer{\Xi \Vdash t :: \Delta X^1. U}
{\Xi \Vdash t :: U & X^1 \notin FV(\Xi)}

&

\infer{\Xi \Vdash t :: [U'/X] U}
{\Xi \Vdash t :: \Delta X^1.U}

%% \infer{\Delta \vdash \lambda y.[t/x]t':S_1 \longrightarrow S_3}{\Delta
%% \vdash \lambda y.t: S_1 \longrightarrow S_2 & \Delta \vdash \lambda x.t': S_2 \longrightarrow S_3}

\end{tabular}
\

\noindent Note that for any $x:y \ep S \in \Gamma$ where $\Gamma \vdash t: t \ep S$, first rename to $x: x \ep S \in \Gamma$, with $\Gamma \vdash \underline{t} : \underline{t} \ep S$ then $x::S \in \Xi$ with $\Xi \Vdash \underline{t}::S$. And $U\ := S \ | \ \Pi x:U.U \ | \ \Delta X^1.U$.
\end{definition}

\begin{definition}
\

  $\interp{S} := S$

  $\interp{\Pi x:U'.U} := \iota f. \forall x. (x \ep \interp{U'} \to f\ x \ep \interp{U})$

  $\interp{\Delta X^1.U} := \iota x. (\Pi X^1. x \ep \interp{U})$
\end{definition}
\begin{theorem}
  If $\Xi \Vdash t:: U$, then $\interp{\Xi} \vdash t: t\ep \interp{U}$.
\end{theorem}
\begin{proof}
  By induction on the derivation. 
\end{proof}
There is no set(by that I means ``set'' itself is not considered a formula), thus there 
is no such thing as Formula-Set reciprocity, it just a coarse approximation of what happen
when we just use internal language to do typing and the Church numerals happens to have a 
special behavior. Thus it is convenient at meta level to abrieviate certain behavior of 
typing as \textit{simple functional language}.    
 
\cite{hatcher:1982}

\bibliographystyle{plain}
\bibliography{invest}


\end{document}
